<html>
<head><meta charset="utf-8"><title>Unsafe and UB · t-lang · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/index.html">t-lang</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html">Unsafe and UB</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="194369269"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194369269" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194369269">(Apr 16 2020 at 21:23)</a>:</h4>
<p>@josh <a href="#narrow/stream/213817-t-lang/topic/values.20of.20Rust/near/194229359" title="#narrow/stream/213817-t-lang/topic/values.20of.20Rust/near/194229359">wrote</a>.</p>
<blockquote>
<blockquote>
<p>it should not be possible to have undefined behavior without the unsafe keyword.</p>
</blockquote>
<p>Is it "undefined behavior" you want to flag here? That statement is true, but it seems somewhat separate from the primary things unsafe exists to address.</p>
<p>I feel like that's related to what unsafe means, but not directly what unsafe means.</p>
</blockquote>
<p>that thread went elsewhere so I am forking here</p>



<a name="194369358"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194369358" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194369358">(Apr 16 2020 at 21:24)</a>:</h4>
<p><span class="user-mention" data-user-id="239881">@Josh Triplett</span> I would have defined exactly that to be the primary concern of <code>unsafe</code> -- to avoid UB.<br>
What would you have said is "directly what unsafe means"?</p>



<a name="194369681"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194369681" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194369681">(Apr 16 2020 at 21:27)</a>:</h4>
<p>At the risk of handwaving on the fly: I feel like <code>unsafe</code> is more closely related to invariants or requirements than to UB specifically.</p>



<a name="194369718"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194369718" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194369718">(Apr 16 2020 at 21:27)</a>:</h4>
<p>An <code>unsafe</code> method on a type isn't necessarily going to produce UB if you call it with insufficient care.</p>



<a name="194369840"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194369840" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194369840">(Apr 16 2020 at 21:28)</a>:</h4>
<p>It might just violate an invariant of the type, or produce an assert or panic, for instance. The existence of a check and panic might prevent any actual UB from occurring, but that doesn't mean the method should be marked safe.</p>



<a name="194370698"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194370698" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Lokathor <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194370698">(Apr 16 2020 at 21:37)</a>:</h4>
<p>well you just marked all of indexing unsafe with that rule :P</p>



<a name="194460996"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194460996" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> mark-i-m <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194460996">(Apr 17 2020 at 15:50)</a>:</h4>
<p>I think I know what Josh is getting at: from an end-user's perspective, I don't really care about UB for its own sake. Rather, I care that my program is correct, fast, and not a pain to write. We define UB in rust to achieve rust's balance of these goals.</p>



<a name="194461453"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194461453" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194461453">(Apr 17 2020 at 15:53)</a>:</h4>
<p>Thinking about it further, I think it's reasonable to describe <code>unsafe</code> as marking regions where the compiler doesn't prevent you from invoking UB (including library UB) and you need to take care not to do so. (Though I'd phrase it somewhat differently when explaining it to a new Rust user than when documenting it for a language definition.) I think there's a certain degree to which I may just be shying away from using "UB" as part of a description of a useful concept, because I've mostly seen "UB" used as a hammer to hit people over the head with and tell them that their programs were never right to begin with so it's OK for the compiler to break them.</p>



<a name="194461478"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194461478" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194461478">(Apr 17 2020 at 15:53)</a>:</h4>
<p>I need to learn that not everyone uses the term "UB" that way.</p>



<a name="194463890"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194463890" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194463890">(Apr 17 2020 at 16:09)</a>:</h4>
<p><span class="user-mention silent" data-user-id="239881">Josh Triplett</span> <a href="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194369681" title="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194369681">said</a>:</p>
<blockquote>
<p>At the risk of handwaving on the fly: I feel like <code>unsafe</code> is more closely related to invariants or requirements than to UB specifically.</p>
</blockquote>
<p>hm, interesting. to me, the purpose of these invariants is to prove absence of UB.</p>



<a name="194463962"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194463962" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194463962">(Apr 17 2020 at 16:10)</a>:</h4>
<p>but of course I come from the perspective of a PL researcher, always on the look for a theorem to prove</p>



<a name="194463991"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194463991" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194463991">(Apr 17 2020 at 16:10)</a>:</h4>
<p>"without unsafe there is no UB" is a really juicy theorem :D</p>



<a name="194464068"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464068" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464068">(Apr 17 2020 at 16:11)</a>:</h4>
<p>do you have interesting examples of invariants people are guarding with <code>unsafe</code> that are unrelated to UB?</p>



<a name="194464215"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464215" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464215">(Apr 17 2020 at 16:12)</a>:</h4>
<p>Offhand, I can think of data structures involving multiple coordinated things and using indexes as "pointers" into a <code>Vec</code> (because you can't have references and the thing they reference in the same <code>struct</code>), where <code>unsafe</code> methods are the ones that don't guarantee every index has a corresponding Vec element.</p>



<a name="194464225"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464225" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464225">(Apr 17 2020 at 16:12)</a>:</h4>
<p>one example I could think of (stealing from PL literature here, people did stuff like that e.g. for Haskell) is having a type that enforces information flow properties, so that no safe program can leak confidential data on untrusted channels. that is another theorem, rather independent from UB.</p>



<a name="194464258"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464258" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464258">(Apr 17 2020 at 16:13)</a>:</h4>
<p>Effectively, data-structure invariants rather than language-level UB. If it were <code>std</code>, we'd call it "library UB".</p>



<a name="194464287"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464287" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464287">(Apr 17 2020 at 16:13)</a>:</h4>
<p><span class="user-mention silent" data-user-id="239881">Josh Triplett</span> <a href="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194464258" title="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194464258">said</a>:</p>
<blockquote>
<p>Effectively, data-structure invariants rather than language-level UB. If it were <code>std</code>, we'd call it "library UB".</p>
</blockquote>
<p>I think user crates can also have "library UB", std is not special here.</p>



<a name="194464416"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464416" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464416">(Apr 17 2020 at 16:14)</a>:</h4>
<p>OK, I can't help but meme here:<br>
"You can't just call everything undefined behavior!"<br>
"haha unsafe go brrr"</p>



<a name="194464426"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464426" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464426">(Apr 17 2020 at 16:14)</a>:</h4>
<p>actually <a href="#narrow/stream/122651-general/topic/Library.20level.20Undefined.20Behavior" title="#narrow/stream/122651-general/topic/Library.20level.20Undefined.20Behavior">this was recently discussed here</a> ;)</p>



<a name="194464468"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464468" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464468">(Apr 17 2020 at 16:14)</a>:</h4>
<p><span class="user-mention silent" data-user-id="239881">Josh Triplett</span> <a href="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194464416" title="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194464416">said</a>:</p>
<blockquote>
<p>OK, I can't help but meme here:<br>
"You can't just call everything undefined behavior!"<br>
"haha unsafe go brrr"</p>
</blockquote>
<p>I got to admit this one is lost on me^^</p>



<a name="194464544"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464544" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464544">(Apr 17 2020 at 16:15)</a>:</h4>
<p>in std I think a long time ago a policy was set not to use <code>unsafe</code> to guard against non-UB "dangerous" API usage. that was when <code>mem::forget</code> became safe.</p>



<a name="194464614"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464614" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464614">(Apr 17 2020 at 16:16)</a>:</h4>
<p>Right. I think it's worth observing that not every library follows the same policy as <code>std</code>.</p>



<a name="194464647"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464647" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464647">(Apr 17 2020 at 16:16)</a>:</h4>
<p>And in particular, I think if I were writing a library crate and there were a method that could leak memory if misused, I'd mark it <code>unsafe</code>.</p>



<a name="194464669"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464669" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464669">(Apr 17 2020 at 16:16)</a>:</h4>
<p>As in "you need to carefully read the requirements of this method before using it, they may not be enforced by the interface".</p>



<a name="194464682"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464682" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464682">(Apr 17 2020 at 16:16)</a>:</h4>
<p>hm, interesting.</p>



<a name="194464720"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464720" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464720">(Apr 17 2020 at 16:17)</a>:</h4>
<p>but I am not sure how common that sentiment is</p>



<a name="194464761"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464761" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464761">(Apr 17 2020 at 16:17)</a>:</h4>
<p>so "unsafe is to prevent UB" might still be the "least common denominator", the one thing we <em>have</em> to all agree on to make the ecosystem work</p>



<a name="194464796"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464796" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464796">(Apr 17 2020 at 16:17)</a>:</h4>
<p>I don't know either. But given that people can define any method as <code>unsafe</code> to call, they can attach any semantic they want to it.</p>



<a name="194464819"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464819" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464819">(Apr 17 2020 at 16:18)</a>:</h4>
<p>that doesn't exclude people from using stronger invariants locally.</p>



<a name="194464941"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464941" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464941">(Apr 17 2020 at 16:18)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194464761" title="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194464761">said</a>:</p>
<blockquote>
<p>so "unsafe is to prevent UB" might still be the "least common denominator", the one thing we <em>have</em> to all agree on to make the ecosystem work</p>
</blockquote>
<p>Right. If something could cause UB, it <em>must</em> be marked as <code>unsafe</code>. But something being marked <code>unsafe</code> doesn't require that it relates to UB.</p>



<a name="194464987"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194464987" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194464987">(Apr 17 2020 at 16:19)</a>:</h4>
<p>Some crates don't actually uphold the guarantees laid down in the Nomicon - "you cannot cause UB without unsafe" - and expose some functions as safe that are possible, but not easy to misuse, because guarding against all misuse is too costly in terms of performance. <code>libc</code> and <code>glium</code> come to mind</p>



<a name="194465177"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465177" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465177">(Apr 17 2020 at 16:20)</a>:</h4>
<p>I'm curious, what kinds of methods in <code>libc</code> potentially allow UB without being <code>unsafe</code>?</p>



<a name="194465195"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465195" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465195">(Apr 17 2020 at 16:20)</a>:</h4>
<p><span class="user-mention" data-user-id="239881">@Josh Triplett</span> that's fair. but even with that I think the relation to UB is so supremely important that it should be part of whatever one-sentence "pitch" about unsafe ends up in a "values" doument.</p>



<a name="194465238"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465238" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465238">(Apr 17 2020 at 16:21)</a>:</h4>
<p><span class="user-mention silent" data-user-id="239881">Josh Triplett</span> <a href="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194465177" title="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194465177">said</a>:</p>
<blockquote>
<p>I'm curious, what kinds of methods in <code>libc</code> potentially allow UB without being <code>unsafe</code>?</p>
</blockquote>
<p><code>fork</code> comes to my mind... I think there's still some crates out there that expose it safely, might not be <code>libc</code>.</p>



<a name="194465288"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465288" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465288">(Apr 17 2020 at 16:21)</a>:</h4>
<p><a href="https://github.com/rust-lang/libc/issues/1501" title="https://github.com/rust-lang/libc/issues/1501">https://github.com/rust-lang/libc/issues/1501</a> for example</p>



<a name="194465296"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465296" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465296">(Apr 17 2020 at 16:21)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> If that's the case, then it needs explanation for the benefit of people who don't know what that document may mean by "UB", or who have different associations with the concept than programming language researchers do. :)</p>



<a name="194465440"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465440" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465440">(Apr 17 2020 at 16:23)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> Before I came to Rust, I understood in general what undefined behavior was, but my association with it very much included a critical subset of "what standards refuse to define despite it having a practical definition in real-world compilers, and which we have to keep passing more options to those compilers to remind them to stop breaking it".</p>



<a name="194465490"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465490" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465490">(Apr 17 2020 at 16:23)</a>:</h4>
<p>oh I see, you are saying the term is burnt for some people</p>



<a name="194465493"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465493" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465493">(Apr 17 2020 at 16:24)</a>:</h4>
<p>yeah I can see that</p>



<a name="194465540"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465540" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465540">(Apr 17 2020 at 16:24)</a>:</h4>
<p>Right.</p>



<a name="194465543"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465543" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465543">(Apr 17 2020 at 16:24)</a>:</h4>
<p>I mean, until some of the most recent C standards, it was UB to assume that integers are two's complement.</p>



<a name="194465580"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465580" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465580">(Apr 17 2020 at 16:24)</a>:</h4>
<p>I agree UB in C is... sad :(</p>



<a name="194465585"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465585" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465585">(Apr 17 2020 at 16:24)</a>:</h4>
<p>which is why I am working hard to make it better in Rust^^</p>



<a name="194465607"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465607" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465607">(Apr 17 2020 at 16:24)</a>:</h4>
<p>And I think it's still UB to cast a pointer to a different type and dereference it, despite that happening <em>all the time</em> in systems programming contexts.</p>



<a name="194465609"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465609" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465609">(Apr 17 2020 at 16:24)</a>:</h4>
<p>maybe we shouldnt have re-used the term</p>



<a name="194465662"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465662" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465662">(Apr 17 2020 at 16:25)</a>:</h4>
<p>the underlying principle is the same but people can see UB in C and put out the baby with the bathwater</p>



<a name="194465669"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465669" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465669">(Apr 17 2020 at 16:25)</a>:</h4>
<p>Yeah.</p>



<a name="194465786"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465786" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465786">(Apr 17 2020 at 16:26)</a>:</h4>
<p>There are a <em>lot</em> of people whose fundamental reasoning is "I know what code this should turn into, and I know what that code does on the machine". Which is sometimes reasonable, and sometimes not.</p>



<a name="194465791"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465791" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465791">(Apr 17 2020 at 16:26)</a>:</h4>
<p>what I mostly dont like about the term is that it's a negative one</p>



<a name="194465853"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465853" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465853">(Apr 17 2020 at 16:26)</a>:</h4>
<p>I'd much rather say "this program is $safe" ($safe := "cannot cause UB"/"has well-defined semantics"/"does not hit an error state in the abstract machine") than "this program is UB-free"</p>



<a name="194465896"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465896" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465896">(Apr 17 2020 at 16:27)</a>:</h4>
<p><span aria-label="+1" class="emoji emoji-1f44d" role="img" title="+1">:+1:</span></p>



<a name="194465908"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194465908" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194465908">(Apr 17 2020 at 16:27)</a>:</h4>
<p>I agree with preferring positive statements to negative ones.</p>



<a name="194466008"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194466008" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194466008">(Apr 17 2020 at 16:28)</a>:</h4>
<p>in PL research we sometimes use "safe" for that, might be confusing though with "safe code"... we'd basically be saying "even your unsafe code must be safe but then it is your responsibility; safe code is checked to be safe by the compiler"^^</p>



<a name="194466355"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194466355" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194466355">(Apr 17 2020 at 16:30)</a>:</h4>
<p>Yeah. I wonder sometimes if there was a term like "unchecked" we could have used instead of "unsafe".</p>



<a name="194466364"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194466364" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> simulacrum <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194466364">(Apr 17 2020 at 16:30)</a>:</h4>
<p>I do think it may be confusing, but can also be helpful. I recall finding it illuminating that "all code must be safe", i.e. that unsafe is not an escape hatch into UB is fine.</p>



<a name="194466392"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194466392" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194466392">(Apr 17 2020 at 16:30)</a>:</h4>
<p>"Abandon all compiler aid, all ye who press enter here"</p>



<a name="194466502"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194466502" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194466502">(Apr 17 2020 at 16:31)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116122">simulacrum</span> <a href="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194466364" title="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194466364">said</a>:</p>
<blockquote>
<p>I do think it may be confusing, but can also be helpful. I recall finding it illuminating that "all code must be safe", i.e. that unsafe is not an escape hatch into UB is fine.</p>
</blockquote>
<p>"statically" and "dynamically" safe woild be possible disambiguations here</p>



<a name="194466724"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194466724" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> simulacrum <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194466724">(Apr 17 2020 at 16:33)</a>:</h4>
<p>Hm, that's an interesting way of looking at it. I think I may like it :)</p>



<a name="194466970"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194466970" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194466970">(Apr 17 2020 at 16:35)</a>:</h4>
<p>Interesting. How does that interact with things like "dynamic" borrow checking, such as <code>Rc</code>?</p>



<a name="194467328"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194467328" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194467328">(Apr 17 2020 at 16:38)</a>:</h4>
<p>hm, if someone said "dynamic borrow checking" I'd think they mean Stacked Borrows as that's how I have sometimes described it^^</p>



<a name="194467353"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194467353" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194467353">(Apr 17 2020 at 16:38)</a>:</h4>
<p>and then it is quite parallel with statically/dynamically "safe" code</p>



<a name="194467412"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194467412" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194467412">(Apr 17 2020 at 16:39)</a>:</h4>
<p><code>Rc</code> has no equivalent to <code>&amp;mut</code>, so I cannot really see it as a "dynamic borrow checker". if anything, that would be <code>RefCell</code>.</p>



<a name="194467449"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194467449" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194467449">(Apr 17 2020 at 16:39)</a>:</h4>
<p>I very much think of stacked borrows as static borrow checking, just <em>smarter</em> static borrow checking.</p>



<a name="194467472"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194467472" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194467472">(Apr 17 2020 at 16:39)</a>:</h4>
<p>but stacked borrows is dynamic</p>



<a name="194467480"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194467480" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194467480">(Apr 17 2020 at 16:39)</a>:</h4>
<p>as in, it runs at "program run-time"</p>



<a name="194467542"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194467542" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194467542">(Apr 17 2020 at 16:40)</a>:</h4>
<p>it's not a static analysis that you can run on code without executing said code</p>



<a name="194467586"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194467586" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194467586">(Apr 17 2020 at 16:40)</a>:</h4>
<p>we have a static analysis that approximates stacked borrows, and it is called borrow checking</p>



<a name="194468088"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468088" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468088">(Apr 17 2020 at 16:44)</a>:</h4>
<p>I wasn't aware of the dynamic version. I thought that stacked borrows was a model that was being used to analyze and reason about the borrow checker.</p>



<a name="194468139"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468139" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468139">(Apr 17 2020 at 16:44)</a>:</h4>
<p>there <em>only</em> is a dynamic version</p>



<a name="194468187"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468187" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468187">(Apr 17 2020 at 16:45)</a>:</h4>
<p>it is a model used to analyze the borrow checker, well, one could say that, but analysis happens by "run this code in miri"</p>



<a name="194468201"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468201" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468201">(Apr 17 2020 at 16:45)</a>:</h4>
<p>/me is confused.</p>



<a name="194468266"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468266" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468266">(Apr 17 2020 at 16:46)</a>:</h4>
<p>I thought that the model was a formal reasoning model, as in a set of written rules and theorems for human readers, not a computer implementation.</p>



<a name="194468308"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468308" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468308">(Apr 17 2020 at 16:46)</a>:</h4>
<p>we can then prove theorems about programs running with stacked borrows, and those theorems are "static" in some sense</p>



<a name="194468314"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468314" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468314">(Apr 17 2020 at 16:46)</a>:</h4>
<p>It's a code implementation, first and foremost?</p>



<a name="194468446"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468446" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468446">(Apr 17 2020 at 16:47)</a>:</h4>
<p>Stacked Borrows is...</p>
<ul>
<li>a code implementation in Miri, that does some extra checking when running Rust code.</li>
<li>a formalization of these rules as a formal "operational semantics".</li>
</ul>
<p>these two are basically equivalent, just one is written in Rust and the other in math/Coq</p>



<a name="194468471"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468471" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468471">(Apr 17 2020 at 16:47)</a>:</h4>
<p>Ah, that makes more sense, thank you. I was only aware of the latter, not the former.</p>



<a name="194468515"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468515" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468515">(Apr 17 2020 at 16:48)</a>:</h4>
<p>and both are "dynamic" in nature</p>



<a name="194468530"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468530" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468530">(Apr 17 2020 at 16:48)</a>:</h4>
<p>in the sense that thy describe program executions</p>



<a name="194468565"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468565" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468565">(Apr 17 2020 at 16:48)</a>:</h4>
<p>you wouldn't call Rust "static" just because there exists a "static" piece of code (Miri) that can run Rust code</p>



<a name="194468622"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468622" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468622">(Apr 17 2020 at 16:49)</a>:</h4>
<p>No, certainly not. I was thinking of the formal model, and then of the borrow-checker rules in Rust that that model models.</p>



<a name="194468626"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468626" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468626">(Apr 17 2020 at 16:49)</a>:</h4>
<p>so likewise, these formal "operational" rules, while being written for human and mathematical consumption, are as "dynamic" as an interpreter</p>



<a name="194468670"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468670" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468670">(Apr 17 2020 at 16:49)</a>:</h4>
<p>they have the same information content</p>



<a name="194468673"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468673" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468673">(Apr 17 2020 at 16:49)</a>:</h4>
<p>Thanks for the explanation and clarification. :)</p>



<a name="194468709"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468709" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468709">(Apr 17 2020 at 16:49)</a>:</h4>
<p>sure. :) I realize I am using a lot of jargon and don't always know which part of it is confusing.</p>



<a name="194468832"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468832" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468832">(Apr 17 2020 at 16:50)</a>:</h4>
<p><span class="user-mention silent" data-user-id="239881">Josh Triplett</span> <a href="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194468314" title="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194468314">said</a>:</p>
<blockquote>
<p>It's a code implementation, first and foremost?</p>
</blockquote>
<p>historical trivia, I did the code implementation first, and then a colleague put everything into math ;)</p>



<a name="194468840"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468840" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468840">(Apr 17 2020 at 16:50)</a>:</h4>
<p>In this case, it wasn't the jargon, just information I was missing about the nature of stacked borrows.</p>



<a name="194468888"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194468888" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194468888">(Apr 17 2020 at 16:51)</a>:</h4>
<p>but in my head both are just different ways to express the same concepts</p>



<a name="194469085"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194469085" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194469085">(Apr 17 2020 at 16:52)</a>:</h4>
<p>that's what I like so much about Miri -- it is an artifact that lets me very clearly communicate details of semantics with people that have no/not much formal background but understand interpreters, and at the same time it is a very precise mathematical specification of Rust behavior, and one that we can even test</p>



<a name="194469243"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194469243" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194469243">(Apr 17 2020 at 16:53)</a>:</h4>
<p>so with my PhD advisor I'd discuss rust semantics via formal mathematical rules, and here on Zulip I'd discuss the same things by pointing at Rust code implementing steps in an interpreter ;)</p>



<a name="194505916"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194505916" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scottmcm <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194505916">(Apr 17 2020 at 22:03)</a>:</h4>
<p>One thing I've found valuable about <code>std</code> keeping a fairly hard line about <code>unsafe</code> meaning that misuse can be unsound is that it reduces the tendency for people to "how bad could it be?"</p>



<a name="194506113"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194506113" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scottmcm <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194506113">(Apr 17 2020 at 22:05)</a>:</h4>
<p>More more APIs that are unsafe for being easy to misuse, the more likely people are to say "I'm pretty sure that this won't be zero, so I'll just use <code>NonZeroU32::new_unchecked</code>; it's just a correctness hint".</p>



<a name="194506338"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194506338" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> simulacrum <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194506338">(Apr 17 2020 at 22:08)</a>:</h4>
<p>I have wanted a separate lint, though likely deny by default, that is basically that middle ground of "be very careful but not UB"</p>



<a name="194528645"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194528645" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Lokathor <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194528645">(Apr 18 2020 at 06:13)</a>:</h4>
<p>I've never marked code as unsafe if i wasn't worried about UB happening, but I've also often wanted "hey watch it with this" signs</p>



<a name="194528709"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194528709" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Lokathor <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194528709">(Apr 18 2020 at 06:15)</a>:</h4>
<p>An attribute on functions that rustdoc knows about and that signals a warning by default seems an appropriate solution to this sort of thing</p>



<a name="194528715"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194528715" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Lokathor <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194528715">(Apr 18 2020 at 06:15)</a>:</h4>
<p>like the reverse of must_use</p>



<a name="194539475"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194539475" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194539475">(Apr 18 2020 at 11:23)</a>:</h4>
<p>Catching up on this thread:</p>
<ul>
<li>I still stand by the principle that <code>unsafe</code> means "you may create UB" full-stop, at least in the stdlib. It seems like a <strong>really important</strong> line to me. To me, it's the difference between writing Java/Python code and writing C++, in some sense, in terms of reliability, and that's a huge difference.</li>
<li>Still, I think that there <em>is</em> a need to be able to mark "dangerous" methods that don't cause UB but may have other consequences. </li>
<li>Of course it's been proposed to let people give "reasons" that things are unsafe, or other details, and maybe that's a good compromise. So <code>unsafe</code> is kind of <code>unsafe(ub)</code> today, and maybe there are other invariants that are threatened. </li>
<li>In practice, safe code <em>can</em> cause UB, yes, the standard example is writing to <code>/proc/mem</code> or whatever. I think that's a tricky line and I don't really know how to think about it, but I suspect I would draw a "harsher" than line than some libraries do. I think we have to be <strong>really, really</strong> careful here. (See above about how big a difference it is.)</li>
<li>I tend to agree the term UB is not great for a variety of reasons. I don't think it sounds as dangerous as it is, for one thing, and I think it's "poisoned" by the way it's been conflated with "implementation dependent" and some other things. It's also not great that it's negative, but sometimes that's useful too (it's useful to be able to say "this is dangerous" and "this is safe", in other words).</li>
</ul>



<a name="194549281"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194549281" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Amanieu <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194549281">(Apr 18 2020 at 15:12)</a>:</h4>
<p>I'm against extending <code>unsafe</code> beyond "you may create UB". That's how we ended up with things like <code>AssertUnwindSafe</code> which I feel is a huge API wart.</p>



<a name="194549841"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194549841" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> simulacrum <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194549841">(Apr 18 2020 at 15:24)</a>:</h4>
<p>Yeah, I would strongly agree about not extending unsafe. I think there may be room for creating something else (different keyword, etc) that is separate, specifically to provide more room for saying "unsafe is just about UB"</p>



<a name="194553129"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194553129" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> mark-i-m <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194553129">(Apr 18 2020 at 16:39)</a>:</h4>
<p>ugh me and my fat fingers</p>



<a name="194553179"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194553179" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> mark-i-m <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194553179">(Apr 18 2020 at 16:40)</a>:</h4>
<p>I like Ralf's description: "safe" = "has well-defined semantics"</p>



<a name="194553186"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194553186" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> mark-i-m <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194553186">(Apr 18 2020 at 16:40)</a>:</h4>
<p>^^^ that's what I meant to type</p>



<a name="194553371"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194553371" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> mark-i-m <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194553371">(Apr 18 2020 at 16:45)</a>:</h4>
<p>I've also really wondered about the practical edge cases in kernel development: in particular, it seems like rust's abstract machine kind of assumes a sane traditional process model in which processes have a normal address space that doesn't change observably during the program. This is absolutely not true for an operating system where parts of the address space may appear or disappear or be modified by hardware (e.g. consider memory-mapped io where a ld/st instruction doesn't mean what it normally means) or paging or switch from 32-bit mode to 64-bit mode... it means that crates like <a href="https://docs.rs/x86_64/0.10.1/x86_64/index.html" title="https://docs.rs/x86_64/0.10.1/x86_64/index.html">x86_64</a> are very hard to make ergonomic because nearly everything can break some assumption about the underlying state of the machine</p>



<a name="194553524"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194553524" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Amanieu <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194553524">(Apr 18 2020 at 16:48)</a>:</h4>
<p>I don't think that Rust's memory model is incompatible with this: such changes are simply concurrent modifications by another "thread" (in this case the MMU). All you need is an appropriate fence (either a <code>compiler_fence</code> or an <code>asm!</code> with the "memory" clobber)  to avoid data races.</p>



<a name="194553778"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194553778" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> mark-i-m <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194553778">(Apr 18 2020 at 16:55)</a>:</h4>
<p><span class="user-mention" data-user-id="143274">@Amanieu</span> I think I agree that it's not incompatible with rust's memory model, but I guess I'm not fully confident that the solution you mentioned is a general solution -- it seems like there could be corner cases. For example, switching modes means that the definition of a pointer changes (64-bit pointers may no longer be valid) and making paging changes may mean that two pointers start aliasing that weren't before. Somehow you need to inform the compiler about that or else use unsafe everywhere... doing it ergonomically is rather hard.</p>



<a name="194585182"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194585182" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194585182">(Apr 19 2020 at 08:03)</a>:</h4>
<p><span class="user-mention silent" data-user-id="143274">Amanieu</span> <a href="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194549281" title="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194549281">said</a>:</p>
<blockquote>
<p>I'm against extending <code>unsafe</code> beyond "you may create UB". That's how we ended up with things like <code>AssertUnwindSafe</code> which I feel is a huge API wart.</p>
</blockquote>
<p><code>AssertUnwindSafe</code> is <em>not</em> unsafe though, so it is explicitly <em>not</em> an example for extending unsafe beyond UB.</p>



<a name="194585185"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194585185" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194585185">(Apr 19 2020 at 08:03)</a>:</h4>
<p><span class="user-mention" data-user-id="198054">@mark-i-m</span> those are some valid and seriously hard questions you are raising there</p>



<a name="194585250"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194585250" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194585250">(Apr 19 2020 at 08:05)</a>:</h4>
<p>in terms of academic PL research, most researchers run away screaming when you ask them about page table changes, so there's not a ton of work in that area. ;) even just precisely specifying hardware behavior of these things, or other things like "what when executing an instructions races with other code that <em>modifies the encoded instruction</em>", is a niche. I know of no work that tries to then push such low-level shenanigans up through a high-level abstract machine.</p>



<a name="194585299"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194585299" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194585299">(Apr 19 2020 at 08:06)</a>:</h4>
<p>do people really switch address mode between 32 and 64 bit <em>in Rust</em>? like, during the execution of a single rust program? that's... wow.^^</p>



<a name="194600134"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194600134" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194600134">(Apr 19 2020 at 14:24)</a>:</h4>
<p>If you're writing an operating system in Rust, sure. You have to.</p>



<a name="194600870"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194600870" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194600870">(Apr 19 2020 at 14:40)</a>:</h4>
<p>I thought this would happen sometime in some assembly-written preamble early in the bootloader or so</p>



<a name="194600877"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194600877" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194600877">(Apr 19 2020 at 14:41)</a>:</h4>
<p>but my thoughts in this area are clearly very naive</p>



<a name="194600881"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194600881" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194600881">(Apr 19 2020 at 14:41)</a>:</h4>
<p>also I forgot about running 32bit programs on a 64bit host...</p>



<a name="194601209"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194601209" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194601209">(Apr 19 2020 at 14:46)</a>:</h4>
<p>That's one case; another is booting a 64-bit OS on 32-bit firmware.</p>



<a name="194601227"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194601227" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194601227">(Apr 19 2020 at 14:47)</a>:</h4>
<p>There will definitely be assembly involved, though.</p>



<a name="194601234"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194601234" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194601234">(Apr 19 2020 at 14:47)</a>:</h4>
<p>For the actual mode switch.</p>



<a name="194601323"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194601323" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194601323">(Apr 19 2020 at 14:49)</a>:</h4>
<p>Entering 64-bit mode requires page tables, and I certainly don't want to construct page tables in assembly. I would rather do that in Rust...</p>



<a name="194601384"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194601384" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194601384">(Apr 19 2020 at 14:50)</a>:</h4>
<p>But at that point I think those might just be separate Rust programs. One compiled as 32-bit and one compiled as 64-bit.</p>



<a name="194611661"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194611661" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> mark-i-m <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194611661">(Apr 19 2020 at 18:32)</a>:</h4>
<p>@RalfJ Hmm... that's good to know.</p>
<p>I am aware of a lot of ongoing work about verifying kernels, file systems, secure enclaves, hypervisors, and hardware (in fact, most recent SOSPs and OSDIs have had at least one track about this). I know they are different problems from specifying an abstract machine (like for a PL), but it seems plausible that work in those areas could be used to inspire an abstract machine specification.  Here is one example of such work: <a href="https://dl.acm.org/doi/10.1145/3132747.3132782" title="https://dl.acm.org/doi/10.1145/3132747.3132782">https://dl.acm.org/doi/10.1145/3132747.3132782</a>. It comes to mind because it talks a bit about some of the crazy things they have to deal with when modeling hardware, and it also shows how they make their proofs scale.</p>
<blockquote>
<p>But at that point I think those might just be separate Rust programs. One compiled as 32-bit and one compiled as 64-bit.</p>
</blockquote>
<p>Actually, this is how I have tried to deal with it (e.g. context-switching). I've tried to set things up so that at the point where weird things happen, it should be "equivalent" to a program ending and another starting. Of course, I don't know if I'm doing it right, which is what prompted my question...</p>



<a name="194725321"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/213817-t-lang/topic/Unsafe%20and%20UB/near/194725321" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/213817-t-lang/topic/Unsafe.20and.20UB.html#194725321">(Apr 20 2020 at 20:01)</a>:</h4>
<p><span class="user-mention silent" data-user-id="143274">Amanieu</span> <a href="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194549281" title="#narrow/stream/213817-t-lang/topic/Unsafe.20and.20UB/near/194549281">said</a>:</p>
<blockquote>
<p>I'm against extending <code>unsafe</code> beyond "you may create UB". That's how we ended up with things like <code>AssertUnwindSafe</code> which I feel is a huge API wart.</p>
</blockquote>
<p><del>I don't think this is a good example -- there is no unsafe required to use that API.</del> I see <span class="user-mention" data-user-id="120791">@RalfJ</span> made this point already, sorry.</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>